More Viable Plasma における exit ゲームの要件
m0t0k1ch1.icon More Viable Plasma の提案の中から exit ゲームに関する部分をピックアップ
---.icon
Exit Game Requirements
We need to formally show our exit game produces the exitable outputs$ E. To help us along the way, we make a few useful definitions.
exit ゲームが exit 可能な出力$ Eを生成することを形式的に示す必要がある。便宜上、いくつかの定義を用いる。
m0t0k1ch1.icon exit 可能な出力はどのように定義されるかという話
Spends
We call two transactions “competing” if they contain any of the same inputs. The list of “competitors” to a transaction is formally defined as follows:
ある 2 つのトランザクションがいくつかの同じ入力を含むとき、それらは「競合している」と呼ぶことにする。あるトランザクションの「競合」は形式的に以下のように定義される。
$ competitors(t) = \{t_i : i \in (0, n\rbrack, I(t_i) \cap I(t) \neq \emptyset\}
m0t0k1ch1.icon 単純に、1 つでも同じ出力を入力として使ってるトランザクションどうしは「競合」
Note that a transaction is a competitor to itself.
あるトランザクションは、自身の競合であることにも注意する。
Canonical Transactions
We call a transaction “canonical” if it’s the first included of any of its competitors.
競合の中で最初にチェーンに含まれたトランザクションを「カノニカル」とする。
m0t0k1ch1.icon これを exit の優先度と混同しないように注意
We define a function that determines which of a set$ Tof transactions came “first”:
トランザクションセット$ Tの中でどのトランザクションが「最初」になるかを決定する関数を以下に定義する。
$ first(T) = t \in T : \forall{t'} \in T, t \neq t', min(O(t)) < min(O(t'))
m0t0k1ch1.icon あるトランザクションセットの中で最も古い出力を持つトランザクションが「最初」
Then we can define a function that takes a transaction and returns whether it’s the “canonical” spend in its set of competitors.
そうすると、あるトランザクションを引数としてそれが競合の中で「カノニカル」かどうかを返す関数を定義できる。
$ canonical : TX \rightarrow bool
$ canonical(t) = (first(competitors(t)) \stackrel?= t)
m0t0k1ch1.icon 「最初」の概念を「競合」するトランザクションセットに適用すると、「カノニカル」が定義できる
Finally, we say that “reality” is the set of canonical transactions for a given Plasma chain.
最後に、「リアリティ」はある Plasma チェーンについてカノニカルなトランザクションセットだと言える。
$ reality(T_n) = \{canonical(t_i) : i \in (0, n\rbrack\}
Unspent, Double Spent
We define two helper functions “unspent” and “double spent”.$ unspenttakes a set of transactions and returns the list of outputs that haven’t been spent.$ double\_spenttakes a list of transactions and returns any outputs that have been used as inputs to more than one transaction.
$ unspentと$ double\_spentという 2 つのヘルパー関数を定義する。$ unspentは、トランザクションセットを引数として未使用な出力のリストを返す。$ double\_spentは、トランザクションセットを引数として 2 つ以上のトランザクションの入力として使用された出力のリストを返す。
First, we define a function$ txo that takes a transaction and returns a list of its inputs and outputs.
まず、トランザクションを引数としてその入力と出力のリストを返す関数$ txoを定義する。
$ txo(t) = O(t) \cup I(t)
Next, we define a function$ TXOthat lists all inputs and outputs for an entire set of transactions:
次に、トランザクションセット内の全ての入力と出力のリストを表す関数$ TXOを定義する。
$ TXO(T_n) = \bigcup^n_{i = 1}txo(t_i)
Now we can define$ unspent:
以上より、$ unspentは以下のように定義できる。
$ unspent(T) = \{o \in TXO(T) : \forall{t} \in T, o \notin I(t)\}
And finally,$ double\_spent:
最後に、$ double\_spentは以下のように定義できる。
$ double\_spent(T) = \{o \in TXO(T) : \exists{t}, t' \in T, t \neq t', o \in I(t) \land o \in I(t')\}
m0t0k1ch1.icon $ \landは論理積（まだ慣れないので、論理和と論理積がどっちがどっちかわからなくなる）
m0t0k1ch1.icon すなわち、$ oが$ I(t)にも$ I(t')にも含まれている場合、正
Requirements
Combining all of these things, we define our function for exitable outputs given a set of transactions,$ E, as:
これら全てを組み合わせると、あるトランザクションセットについて exit 可能な出力$ Eを表す関数は以下のように定義できる。
$ E(T_n) = unspent(reality(T_n)) \setminus double\_spent(T_n)
m0t0k1ch1.icon $ \setminusは差集合
Basically, the set of exitable outputs are the outputs that are part of a canonical transaction, are unspent, and were not spent in two or more non-canonical transactions. This last part effectively punishes users for double spending.
基本的に、exit 可能な出力は、カノニカルなトランザクションに含まれる未使用な出力であり、2 つ以上のカノニカルでないトランザクションで使用されていない。この最後の部分によって、double spend を行ったユーザーは効率よく処罰される。
---.icon
Satisfies Properties
This next section demonstrates that the function described above satisfies the desired properties of safety and liveness.
このセクションでは、上記の仕様が safety と liveness に関する所望の性質を満たすことを示す。
m0t0k1ch1.icon 「上記の仕様」というのは、主に$ E(T_n) = unspent(reality(T_n)) \setminus double\_spent(T_n)のこと
Safety
Our safety property says:
safety は以下である。
$ \forall o \in E(T_n), o \notin I(t_{n + 1}) \Rightarrow o \in E(T_{n + 1})
So to prove this for our$ E(T_n), let's take some$ o \in E(T_n). From our definition,$ omust be in$ unspent(reality(T_n)), and must not be in$ double\_spent(T_n).
$ E(T_n)についてこれを証明するため、$ o \in E(T_n)を考える。定義より、$ oは$ unspent(reality(T_n))に含まれなければならず、$ double\_spent(T_n)に含まれてはいけない。
$ o \notin I(t_{n + 1})means that$ owill still be in$ reality, because only a transaction spending$ ocan impact its inclusion in$ reality. Also,$ ocan't be spent (or double spent) if it wasn't used as an input. So our function is safe!
$ o \notin I(t_{n + 1})は$ oが$ realityであり続けることを意味する。なぜなら、$ oを使用するトランザクションのみが$ realityの内容に影響を与えることができるから。$ oが$ t_{n + 1}の入力でなかった場合、$ oは使用されない（もしくは double spend されない）。
m0t0k1ch1.icon 使用されなかったら exit 可能であり続けるよねということ
Liveness
Our liveness property states:
liveness は以下である。
$ \forall{o} \in E(T_n), o \in I(t_{n + 1}) \Rightarrow o \in E(T_{n + 1}) \oplus O(t_{n + 1}) \subseteq E(T_{n + 1})
However, we do have a case for which liveness does not hold - namely that if the second transaction is a non-canonical double spend, then both the input and all of the outputs will not be exitable. This is a result of the$ double\_spent(T_n)clause. We think this is fine, because it means that only double spent inputs are at risk of being “lost”.
しかし、liveness が成立しないケースが存在する。つまり、2 番目のトランザクションがカノニカルでない double spend な場合、その入力と全ての出力は exit できなくなってしまう。これは$ double\_spent(T_n)の定義から導かれる。「ロスト」するリスクを孕んでいるのは double spent された入力だけなので、これは問題ないとは思う。
The updated property is therefore:
これを加味すると、正しくは以下のようになる。
$ \forall o \in E(T_n), o \in I(t_{n + 1}) \Rightarrow o \in E(T_{n + 1}) \oplus O(t_{n + 1}) \subseteq E(T_{n + 1}) \oplus o \in double\_spent(T_{n + 1})
This is more annoying to prove, because we need to show each implication holds separately, but not together. Basically, given$ \forall o \in E(T_n), o \in I(t_{n + 1}), we need:
これを証明するのは先ほどより厄介である。なぜなら、それぞれの状態が独立していることを示す必要があるから。基本的には、$ \forall o \in E(T_n), o \in I(t_{n + 1})のときに以下が成り立つ必要がある。
$ o \in E(T_{n + 1}) \Rightarrow O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset \land o \notin double\_spent(T_{n + 1})
and
$ O(t_{n + 1}) \subseteq E(T_{n + 1}) \Rightarrow o \notin E(T_{n + 1}) \land o \notin double\_spent(T_{n + 1})
and
$ o \in double\_spent(T_{n + 1}) \Rightarrow O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset \land o \notin E(T_{n + 1})
Let's show the first.$ o \in I(t_{n + 1})means$ owas spent in$ t_{n + 1}. However,$ o \in E(T_{n + 1})means that it's unspent in any canonical transaction. Therefore,$ t_{n + 1}cannot be a canonical transaction.$ O(t_{n + 1}) \cap E(T_{n + 1})is empty if$ t_{n + 1}is not canonical, so we've shown the half. Our specification states that$ o \in double\_spent(T_{n + 1}) \Rightarrow o \notin E(T_{n + 1}), so we can show the second half by looking at the contrapositive of that statement$ o \in E(T_{n + 1}) \Rightarrow o \notin double\_spent(T_{n + 1}).
1 つ目について示す。$ o \in I(t_{n + 1})は$ oが$ t_{n + 1}で使用されたことを意味する。しかし、$ o \in E(T_{n + 1})は、それが全てのカノニカルなトランザクションで使用されていないことを意味する。すなわち$ t_{n + 1}はカノニカルではない。$ t_{n + 1}がカノニカルでない場合、$ O(t_{n + 1}) \cap E(T_{n + 1})は空である。これで半分が証明できた。我々の仕様だと、$ o \in double\_spent(T_{n + 1}) \Rightarrow o \notin E(T_{n + 1})であるので、これの対偶である$ o \in E(T_{n + 1}) \Rightarrow o \notin double\_spent(T_{n + 1})を考えることで残りの半分も証明できる。
m0t0k1ch1.icon 前半：「$ oは$ t_{n + 1}で使用されたが、カノニカルなトランザクションで使用されたわけではない」ということは、$ t_{n + 1}はカノニカルではない、すなわち$ O(t_{n + 1})は exit 可能ではないため、$ O(t_{n + 1}) \cap E(T_{n + 1}) = \emptysetとなる
m0t0k1ch1.icon 後半：$ o \in double\_spent(T_{n + 1}) \Rightarrow o \notin E(T_{n + 1})という仕様の対偶
Next, we'll show the second statement.$ O(t_{n + 1}) \subseteq E(T_{n + 1})implies that$ t_{n + 1} is canonical. If $ t_{n + 1}is canonical, and$ ois an input to$ t_{n + 1}, then$ ois no longer unspent, and therefore$ o \notin E(T_{n + 1}). If$ tis canonical then there cannot exist another earlier spend of the input, so$ o \notin double\_spent(T_{n + 1}).
次に、2 つ目について示す。$ O(t_{n + 1}) \subseteq E(T_{n + 1})は、$ t_{n + 1}がカノニカルだということを意味する。$ t_{n + 1}がカノニカルかつ$ oが$ t_{n + 1}の入力である場合、$ oは未使用ではない。よって、$ o \notin E(T_{n + 1})となる。$ tがカノニカルな場合、その入力を使用するより古いトランザクションは存在しないため、$ o \notin double\_spent(T_{n + 1})となる。
m0t0k1ch1.icon 後半：最新のトランザクションである$ t_{n + 1}がカノニカルなので$ o \notin double\_spent(T_{n + 1})となる
Now the third statement.$ o \in double\_spent(T_{n + 1})means$ tis necessarily not canonical, so we have$ O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset. It also means that$ o \notin E(T_{n + 1})because of our$ \setminus double\_spent(T_n)clause.
3 つ目について。$ o \in double\_spent(T_{n + 1})は、$ tがカノニカルでないことを意味するので$ O(t_{n + 1}) \cap E(T_{n + 1}) = \emptysetとなるし、$ \setminus double\_spent(T_n)節より、$ o \notin E(T_{n + 1})ということも意味している。
m0t0k1ch1.icon 後半：$ E(T_n) = unspent(reality(T_n)) \setminus double\_spent(T_n)の後半部分より自明
Finally, we’ll show that at least one of these must be true. Let’s do a proof by contradiction. Assume the following:
最後に、少なくともこれらのうちのどれか 1 つが真となることを示す。背理法でやってみよう。以下を仮定する。
$ O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset \land o \notin E(T_{n + 1}) \land o \notin double\_spent(T_{n + 1})
m0t0k1ch1.icon これが真の場合、$ o \in E(T_{n + 1})と$ O(t_{n + 1}) \subseteq E(T_{n + 1})と$ o \in double\_spent(T_{n + 1})の全てが偽であるということ
m0t0k1ch1.icon すなわち、これが真のときに矛盾が生じることを示せれば、命題が証明できたことになる（はず）
We’ve already shown that:
既に以下は示されている。
$ o \in E(T_{n + 1}) \Rightarrow O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset \land o \notin double\_spent(T_{n + 1})
We can negate this statement to find:
これを否定することで、以下が求まる。
$ o \notin E(T_{n + 1}) \land (O(t_{n + 1}) \subseteq E(T_{n + 1}) \lor o \in double\_spent(T_{n + 1}))
However, we assumed that:
しかし、我々は以下を仮定している。
$ O(t_{n + 1}) \cap E(T_{n + 1}) = \emptyset \land o \notin double\_spent(T_{n + 1})
Therefore we’ve shown the statement by contradiction.
よって、矛盾が生じるので、命題が示されたことになる。
m0t0k1ch1.icon ムムム？なぜこの流れで背理法による証明が成立したことになるのか理解できてない気がする
m0t0k1ch1.icon 最初の仮定をベースとすると、証明済みである 3 つの命題（の対偶）がどれも成り立たないから矛盾ってこと？
Note that this means we should be careful to ensure that users don’t double spend. Imagine the following scenario:
これは、ユーザーが double spend しないことを慎重に保証すべきだということを意味する。以下のシナリオを想像してみよう。
1. Alice (UTXO1) and Bob (UTXO2) sign a transaction spending to Carol (TX1)
2. Bob (UTXO2) signs a transaction spending to Dan (TX2). This transaction is included first.
3. Alice (UTXO1) sees Bob’s transaction and signs a separate transaction spending to Carol (TX3).
4. The operator then includes TX1 and TX3. The chain is now byzantine and UTXO1 is also locked.
1. Alice（UTXO1）と Bob（UTXO2）が、Carol への送金トランザクション（TX1）に署名する
2. Bob（UTXO2）が Dan への送金トランザクション（TX2）に署名する
このトランザクションが最初にチェーンに含まれたとする
3. Alice（UTXO1）は Bob のトランザクションを見て、別の Carol への送金トランザクション（TX3）に署名する
4. オペレータが TX1 と TX3 をチェーンに含める
チェーンはビザンチンになってしまい、UTXO1 もロックされてしまう
We can mitigate the above example by including timeouts on transactions. TX1 could have an n-block timeout, after which it’s treated like a totally invalid transaction that can’t be used to exit, challenge, or spend.
トランザクションにタイムアウトを含めることで、上記の問題を緩和することができる。例えば TX1 を n ブロック後にタイムアウトさせれば、exit や challenge にも使えず、使用もできない完全に無効なトランザクションとして扱われるだろう。